T:Type, L:(T List). no_repeats(T;rev(L))  no_repeats(T;L) 

latex

Definitions	last(L), P  Q, left + right, x:A. B(x), , {i..j}, {x:A| B(x)} , , i  j < k, #$n, A  B, a < b, s ~ t, l[i], i z j, i <z j, hd(l), Void, A c B, False, l_disjoint(T;l1;l2), A, (x  l), {T}, A List, , rev(as), [car / cdr], as @ bs, P & Q, x:A  B(x), P  Q, P  Q, s = t, t  T, [], Type, x:A. B(x), P  Q, no_repeats(T;l), x:AB(x), type List
Lemmas	iff wf, no repeats wf, not wf, l member wf, rev implies wf, no repeats-append, iff functionality wrt iff, guard wf, l disjoint wf, no repeats cons, false wf, l disjoint singleton, nil member, not functionality wrt iff, no repeats nil, le wf, member wf, int seg wf, nat wf, select member, l member subtype, member-reverse